Nuprl Lemma : w-discrete_wf
11,40
postcript
pdf
w
:World,
i
,
x
:Id. discrete(
i
;
x
)
latex
Definitions
,
x
:
A
B
(
x
)
,
World
,
x
:
A
B
(
x
)
,
discrete(
i
;
x
)
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
t
T
,
Id
Lemmas
Id
wf
,
world
wf
origin
w:World, i, x:Id. discrete(i;x) 
w:World, i, x:Id. discrete(i;x) 
B(x)
B(x)x:A. B(x) T